The present invention relates generally to a technology supporting a program development, and more particularly to a verifying method and a verifying system suitable for detecting a fault of a program so called a bug.
The following two technologies may be typical examples of this type of system for verifying an operation of the program. One technology is a system that verifies the program by actually running the program. This system checks whether or not there is a program operation that might become a factor of fault such as an illicit access to a memory area and so on during the operation of the program.
According to another technology, this kind of verification is carried out before executing the program. This verifying system checks whether or not a description of the program accords with the syntax of a predetermined program language as done by a lint command in, e.g., a UNIX operating system.
The conventional technologies described above, however, have the following problems. That is, according to the method of verifying the program by actually running the program, verifying targets are not all the steps but only steps of the program which have actually been executed. Besides, it is difficult to verify the program with respect to all of combinations of branch conditions. Further, test data for verifying the program are normally manually prepared, and therefore an artificial mistake such as an omission of checking an important portion is easy to induce.
Moreover, even if a verified result is normal in verification as to whether or not the program accords with the syntax of the program language, this result is nothing but to verify that the source program is described based on the predetermined syntax. Namely, it is not checked whether the program operation is normal or not.
What is examined under such circumstances is a system for storing a computer with a request specification of each individual program and automatically checking whether or not this specification properly reflects in the program. The request specification, however, depends on an applied field at which the individual program aims and on functions that should be actualized, and it has been therefore considered difficult to develop a general-purpose program verifying system.
It is a primary object of the present invention to provide a method of and a system for automatically verifying a request specification of a program by a computer, and a general-purpose program verifying technology capable of obviating the problems inherent in the prior art described above.
Namely, according to the present invention, common portions of particular specifications possessed by the respective programs are previously prescribed as a verifying specification. Then, the present invention obviates the above problems by automatically extracting particular specifications (process specifications) possessed by the respective programs which correspond to the verifying specification.
To accomplish the above object of the present invention, according to one aspect of the present invention, a method of verifying an execution program executed by a computer or a source program for generating the execution program, comprises an operation of segmenting the execution program or the source program into blocks each consisting of one or more processes and defined as a part of the program, which correspond to a verifying specification for verifying the program, an operation of generating a plurality of combinations of the two or more blocks as a check route corresponding to the verifying specification, and an operation of extracting the processes corresponding to the verifying specification executed in a predetermined number or greater number of check routes, as a process specification that should be executed also in other check routes, thereby verifying the program.
The verifying method may further comprise an operation of detecting a fault of the program by inspecting a check route in which the processes extracted as the process specification are not executed.
The verifying method may further comprise an operation of displaying the blocks, the check routes and the processes extracted as the process specification or the processes which are not extracted as the process specification.
The verifying method may further comprise an operation of inputting information on the processes constituting a part or the whole of the process specification, as auxiliary information.
Next, the system according to the present invention will be explained in comparison with the prior art system. FIG. 1 is a conceptual diagram for comparing a system architecture of the present invention with the prior art system architecture.
Herein, examples A and B of the verifying specification are given as below. Further, corresponding process specifications a1, a2 and b1, b2 are also exemplified.
Example A: When dealing with a specified program resource in one single function, a process to be paired is needed.
Process specification al: Processes to be paired, which corresponds to acquisition/release of a data buffer exist within one function.
Process specification a2: When operating an execution level (a degree of priority compared with other programs when executing the program) within one single function, a process of raising the execution level and a process of lowering the execution level are paired and exist in this form.
Verifying specification B: When the function is called, parameter elements that must be set are predetermined.
Process specification b1: When a function 1 is called, parameter elements 1, 2, 3, . . . must have been set.
Process specification b2: When a function 2 is called, parameter elements a, b, c, . . . must have been set.
As can be understood from FIG. 1, it is required in the prior art that input values based on individual process specifications be prepared as test data, or the process specifications be held beforehand inside the verifying system.
By contrast, according to the present invention, what is more general-purposed as a specification that should be checked, is previously prepared. Then, the verifying system itself automatically extracts a particular specification from a result of comparisons in a plurality of check routes. Accordingly, it is feasible to provide a more general-purposed system than by the prior art.
As described above, according to the present invention, an execution program executed by a computer or a source program for generating the execution program is segmented into blocks each consisting of one or more processes and defined as a part of the program, which correspond to a verifying specification. A plurality of combinations of the two or more blocks are generated as a check route corresponding to the verifying specification, and the processes corresponding to the verifying specification executed in a predetermined number or greater number of check routes are extracted as a process specification that should be executed also in other check routes, thereby verifying the program. Therefore, the process specification that should be essentially actualized by the individual program is extracted, and a part of the program which does not accord with the process specification, can be automatically extracted.